Nuprl Lemma : rel_exp_functionality_wrt_breqv
11,40
postcript
pdf
n
:
,
T
:Type,
R1
,
R2
:(
T
T
). (
R1
<
>{
T
}
R2
)
(rel_exp(
T
;
R1
;
n
) <
>{
T
} rel_exp(
T
;
R2
;
n
))
latex
Definitions
{
x
:
A
|
B
(
x
)}
,
,
A
B
,
A
,
False
,
E
<
>{
T
}
E'
,
x
:
A
B
(
x
)
,
,
Type
,
,
t
T
,
rel_exp(
T
;
R
;
n
)
,
x
:
A
.
B
(
x
)
,
P
Q
Lemmas
binrel
le
weakening
,
binrel
eqv
inversion
,
rel
exp
functionality
wrt
brle
,
rel
exp
wf
,
binrel
le
antisymmetry
,
nat
wf
,
binrel
eqv
wf
origin
n:
, T:Type, R1, R2:(T
T
). (R1 <
>{T} R2) 
(rel_exp(T;R1;n) <>{T} rel_exp(T;R2;n)) n:, T:Type, R1, R2:(TT). (R1 <>{T} R2) (rel_exp(T;R1;n) <>{T} rel_exp(T;R2;n)) 
B
A>{T} E'B(x)
Tx:A. B(x) Q